package tr.edu.ege.kipler.satisfiability.completion.rules.dl;

import java.util.HashSet;
import java.util.Iterator;
import java.util.Set;

import tr.edu.ege.kipler.satisfiability.UnsatisfiableException;
import tr.edu.ege.kipler.satisfiability.blocking.BlockingStrategy;
import tr.edu.ege.kipler.satisfiability.container.ABox;
import tr.edu.ege.kipler.satisfiability.container.ConceptCategory;
import tr.edu.ege.kipler.satisfiability.container.Individual;
import tr.edu.ege.kipler.satisfiability.container.WcsData;
import tr.edu.ege.kipler.satisfiability.container.operational.DisjointIndividualDetector;
import tr.edu.ege.kipler.satisfiability.container.operational.IndividualNameManager;
import tr.edu.ege.kipler.satisfiability.container.operational.RelatedIndividualWithTypeFilter;
import tr.edu.ege.kipler.syntax.atomicformula.ConceptAssertion;
import tr.edu.ege.kipler.syntax.atomicformula.Formula;
import tr.edu.ege.kipler.syntax.atomicformula.ObjectRoleAssertion;
import tr.edu.ege.kipler.syntax.atomicformula.SameIndividualAssertion;
import tr.edu.ege.kipler.syntax.concept.Concept;
import tr.edu.ege.kipler.syntax.concept.QualifiedNoRestriction;

/**
 * 
 * @author İnanç Seylan
 *
 */
public class AtLeastRule extends ABoxRule {
	private ABox aBox;

	private boolean applied, exhaustive;

	private QualifiedNoRestriction qr;

	private BlockingStrategy blocking;

	private RelatedIndividualWithTypeFilter filter;

	public AtLeastRule(BlockingStrategy blocking,
			RelatedIndividualWithTypeFilter filter, boolean exhaustive) {
		setBlocking(blocking);
		setFilter(filter);
		setExhaustive(exhaustive);
	}

	public RelatedIndividualWithTypeFilter getFilter() {
		return filter;
	}

	public void setFilter(RelatedIndividualWithTypeFilter filterer) {
		this.filter = filterer;
	}

	public BlockingStrategy getBlocking() {
		return blocking;
	}

	public void setBlocking(BlockingStrategy blocking) {
		this.blocking = blocking;
	}

	public boolean isApplied() {
		return applied;
	}

	public boolean isExhaustive() {
		return exhaustive;
	}

	public void setExhaustive(boolean exhaustive) {
		this.exhaustive = exhaustive;
	}

	private boolean atLeastMustBeApplied(ABox aBox, Individual indv) {
		boolean apply = true;
		RelatedIndividualWithTypeFilter filterer = getFilter();
		filterer.setABox(aBox);
		filterer.setIndividual(indv);
		filterer.setRole(qr.getRole());
		filterer.setConcept(qr.getConcept());
		Set<Individual> neighbors = filterer.filter();
		if (neighbors.size() >= qr.getNo()) {
			DisjointIndividualDetector detector = new DisjointIndividualDetector(
					aBox, neighbors);
			apply = !detector.hasSetWithMinCardinality(qr.getNo());
		}
		return apply;
	}

	@Override
	public void apply() throws UnsatisfiableException {
		applied = false;
		aBox = getWorld().getABox();
		if (!getBlocking().isBlocked(aBox, getIndividual().getName())) {
			for (Iterator<Concept> i = getIndividual().conceptIterator(
					ConceptCategory.AT_LEAST); i.hasNext()
					&& ((!isExhaustive() && !isApplied()) || isExhaustive());) {
				Concept concept = i.next();
				qr = (QualifiedNoRestriction) concept;
				if (atLeastMustBeApplied(aBox, getIndividual())) {
					Set<Individual> newFillers = new HashSet<Individual>();
					for (int j = 0; j < qr.getNo(); j++) {
						String newIndvName = IndividualNameManager
								.getInstance().generateIndividualName();
						WcsData wcsData = getWcs().getData();
						Formula depFormula = new ConceptAssertion(qr,
								getIndividual().getName());
						ObjectRoleAssertion or = new ObjectRoleAssertion(qr
								.getRole(), getIndividual().getName(),
								newIndvName);
						wcsData.getDependencyManager().move(or, depFormula);
						ConceptAssertion ca = new ConceptAssertion(qr
								.getConcept(), newIndvName);
						wcsData.getDependencyManager().move(ca, depFormula);
						wcsData.getLogger().info(
								"WCS " + getWcs().getId()
										+ " At least rule: Adding " + ca
										+ " and " + or);
						aBox.add(or);
						aBox.add(ca);
						Individual successor = aBox.getIndividual(newIndvName);
						assertDifferent(successor, newFillers);
						newFillers.add(successor);
					}
					applied = true;
				}
			}
		}
	}

	private void assertDifferent(Individual indv1, Set<Individual> individuals)
			throws UnsatisfiableException {
		for (Individual indv2 : individuals) {
			SameIndividualAssertion ia = new SameIndividualAssertion(indv1
					.getName(), indv2.getName()).toggleNegated();
			if (!indv1.equals(indv2) && !aBox.contains(ia)) {
				WcsData wcsData = getWcs().getData();
				wcsData.getDependencyManager().move(ia,
						new ConceptAssertion(qr, getIndividual().getName()));
				aBox.add(ia);
				wcsData.getLogger().info(
						"WCS " + getWcs().getId() + " At least rule: Adding "
								+ ia);
			}
		}
	}
}
